/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BDR30/FONT#2=BAXM30/FONT#3=BASB30/FONT#4=BDR30/FONT#5=SUB/FONT#6=SUP/FONT#9=FIX40/FONT#10=FIX30/FONT#11=GRFX25/FONT#12=GRFX35
␈↓ ↓H␈↓␈↓ εP␈↓ :75


␈↓ ↓H␈↓β␈↓ ¬tCHAPTER V

␈↓ ↓H␈↓β␈↓ ∧0PROVING LISP PROGRAMS CORRECT




␈↓ ↓H␈↓        In␈αthis␈αchapter␈αwe␈αwill␈αintroduce␈αtechniques␈αfor␈αproving␈αLISP␈αprograms␈αcorrect.␈α In␈αgeneral,
␈↓ ↓H␈↓they will be limited to clean LISP programs.

␈↓ ↓H␈↓        The␈α necessary␈αbasic␈αfacts␈αcan␈αbe␈αdivided␈αinto␈αfour␈αcategories:␈αalgebraic␈αfacts␈αabout␈αlists␈αand
␈↓ ↓H␈↓S-expressions,␈α∞general␈α∞facts␈α∞about␈α∞composition,␈α∞facts␈α∞about␈α∞first␈α∞order␈α∞logic␈α∂including␈α∞conditional
␈↓ ↓H␈↓expressions,␈αfacts␈α
about␈αthe␈α
inductive␈αstructure␈α
of␈αlists␈α
and␈αS-expressions,␈α
and␈αgeneral␈α
facts␈αabout
␈↓ ↓H␈↓functions␈α∞defined␈α
by␈α∞recursion.␈α
 Ideally,␈α∞we␈α∞would␈α
use␈α∞a␈α
general␈α∞theory␈α
of␈α∞recursive␈α∞definition␈α
to
␈↓ ↓H␈↓prove␈αtheorems␈αabout␈αLISP␈αfunctions.␈α However,␈αthe␈αgeneral␈αtheory␈αis␈αnot␈αwell␈αenough␈αdeveloped,
␈↓ ↓H␈↓so␈αwe␈α
have␈αhad␈αto␈α
introduce␈αsome␈αmethods␈α
limited␈αto␈αLISP␈α
functions␈αdefined␈αby␈α
particular␈αkinds
␈↓ ↓H␈↓of recursion schemes.



␈↓ ↓H␈↓1.  ␈↓βAlgebraic facts about S-expressions and lists.␈↓


␈↓ ↓H␈↓        The␈α⊂algebraic␈α⊂facts␈α⊂about␈α⊂S-expressions␈α⊂are␈α∂expressed␈α⊂by␈α⊂the␈α⊂following␈α⊂sentences␈α⊂of␈α∂first
␈↓ ↓H␈↓order logic:

␈↓ ↓H␈↓        ␈↓α∀x.(issexp x ⊃ ␈↓βat␈↓α x ∨ (issexp ␈↓βa␈↓α x ∧ issexp ␈↓βd␈↓α x ∧ x = (␈↓βa␈↓α x . ␈↓βd␈↓α x)))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓α∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬␈↓βat␈↓α(x.y) ∧ x = ␈↓βa␈↓α(x.y) ∧ y = ␈↓βd␈↓α(x.y))␈↓.

␈↓ ↓H␈↓These␈α∞axioms␈α
treat␈α∞S-expressions␈α
among␈α∞other␈α
objects.␈α∞ If␈α
we␈α∞can␈α
assume␈α∞that␈α
all␈α∞objects␈α∞are␈α
S-
␈↓ ↓H␈↓expressions␈α
or␈α
can␈αdeclare␈α
certain␈α
variables␈αas␈α
ranging␈α
only␈α
over␈αS-expressions,␈α
we␈α
can␈αsimplify␈α
the
␈↓ ↓H␈↓axioms to

␈↓ ↓H␈↓        ␈↓α∀x.[␈↓βat␈↓α x ∨ x = [␈↓βa␈↓α x . ␈↓βd␈↓α x]]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓α∀x y.[¬␈↓βat␈↓α[x.y] ∧ x = ␈↓βa␈↓α[x.y] ∧ y = ␈↓βd␈↓α[x.y]]␈↓.

␈↓ ↓H␈↓        The algebraic facts about lists are expressed by the following sentences of first order logic:

␈↓ ↓H␈↓        ␈↓α∀x. islist x ⊃ x = ␈↓∧NIL␈↓α ∨ islist ␈↓βd ␈↓αx␈↓,

␈↓ ↓H␈↓        ␈↓α∀x y. islist y ⊃ islist[x . y]␈↓,
␈↓ ↓H␈↓␈↓ ¬pCHAPTER V␈↓ :76


␈↓ ↓H␈↓        ␈↓α∀x y. islist y ⊃ ␈↓βa␈↓α[x . y] = x ∧ ␈↓βd␈↓α[x.y] = y␈↓,



␈↓ ↓H␈↓2.  ␈↓βStructural Induction␈↓


␈↓ ↓H␈↓